es:ES, x, free:Id, e:E.
@loc(e)(x:Id)
 (((x after e) = (x when e)  Id))
 (0 < round(e))
 (e':E
 ((e' loc e 
 (& rank(e') = <round(e), 0>  (:  )
 (& (((x after e') = (x when e')  Id)))) 

latex

Definitions

inc-snd(p), {T}, SQType(T), ff, S  T, False, A  B, tt, inc-fst(p), let x = a in b(x), if b then t else f fi , Y, t.1, rank(e), , x(s), True, T, round(e), A, P  Q, A c B, x. t(x), , t  T, (e <loc e'), e loc e' , P & Q, x:A. B(x), @i(x:T), P  Q, x:A. B(x), t.2, @e(xv), P  Q, Unit, , Dec(P), WellFnd{i}(A;x,y.R(x;y)),

Lemmas

Id sq, pi2 wf, nat sq, es-le weakening, es-locl transitivity1, inc-snd wf, es-le wf, change-to-last-change, last-change-property, bool sq, bool cases, eq id wf, not functionality wrt iff, assert of bnot, eqff to assert, bnot wf, last-change wf, inc-fst wf, le wf, loc-last-change, assert-eq-id, eqtt to assert, iff transitivity, bool wf, id-deq wf, changed wf, es-le weakening eq, true wf, squash wf, pi1 wf, event system wf, Id wf, es-causl wf, es-loc wf, nat wf, decidable equal Id, es-dtype wf, es-le-loc, f-rank wf, es-locl wf, f-round wf, es-when wf, es-after wf, not wf, es-vartype wf, es-isconst wf, assert wf, es-locl-wellfnd